'Weak Dependency Graph [60.0]' ------------------------------ Answer: YES(?,O(n^1)) Input Problem: innermost runtime-complexity with respect to Rules: { app(nil(), xs) -> nil() , app(cons(x, xs), ys) -> cons(x, app(xs, ys))} Details: We have computed the following set of weak (innermost) dependency pairs: { app^#(nil(), xs) -> c_0() , app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} The usable rules are: {} The estimated dependency graph contains the following edges: {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} ==> {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} ==> {app^#(nil(), xs) -> c_0()} We consider the following path(s): 1) { app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys)) , app^#(nil(), xs) -> c_0()} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: app(x1, x2) = [0] x1 + [0] x2 + [0] nil() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] app^#(x1, x2) = [0] x1 + [0] x2 + [0] c_0() = [0] c_1(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {app^#(nil(), xs) -> c_0()} Weak Rules: {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} Details: We apply the weight gap principle, strictly orienting the rules {app^#(nil(), xs) -> c_0()} and weakly orienting the rules {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {app^#(nil(), xs) -> c_0()} Details: Interpretation Functions: app(x1, x2) = [0] x1 + [0] x2 + [0] nil() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [0] app^#(x1, x2) = [1] x1 + [1] x2 + [1] c_0() = [0] c_1(x1) = [1] x1 + [0] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: { app^#(nil(), xs) -> c_0() , app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} Details: The given problem does not contain any strict rules 2) {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} The usable rules for this path are empty. We have oriented the usable rules with the following strongly linear interpretation: Interpretation Functions: app(x1, x2) = [0] x1 + [0] x2 + [0] nil() = [0] cons(x1, x2) = [0] x1 + [0] x2 + [0] app^#(x1, x2) = [0] x1 + [0] x2 + [0] c_0() = [0] c_1(x1) = [0] x1 + [0] We have applied the subprocessor on the resulting DP-problem: 'Weight Gap Principle' ---------------------- Answer: YES(?,O(n^1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} Weak Rules: {} Details: We apply the weight gap principle, strictly orienting the rules {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} and weakly orienting the rules {} using the following strongly linear interpretation: Processor 'Matrix Interpretation' oriented the following rules strictly: {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} Details: Interpretation Functions: app(x1, x2) = [0] x1 + [0] x2 + [0] nil() = [0] cons(x1, x2) = [1] x1 + [1] x2 + [8] app^#(x1, x2) = [1] x1 + [1] x2 + [1] c_0() = [0] c_1(x1) = [1] x1 + [3] Finally we apply the subprocessor 'Empty TRS' ----------- Answer: YES(?,O(1)) Input Problem: innermost DP runtime-complexity with respect to Strict Rules: {} Weak Rules: {app^#(cons(x, xs), ys) -> c_1(app^#(xs, ys))} Details: The given problem does not contain any strict rules